(declare-fun _substvar_1349_ () Int)
(declare-fun _substvar_1375_ () Int)
(declare-fun _substvar_643_ () Int)
(declare-fun _substvar_827_ () Int)
(declare-fun _substvar_632_ () Int)
(declare-fun _substvar_825_ () Int)
(declare-fun _substvar_830_ () Int)
(declare-fun _substvar_1433_ () Int)
(declare-fun _substvar_625_ () Int)
(declare-fun _substvar_1366_ () Int)
(declare-fun _substvar_641_ () Int)
(declare-fun _substvar_631_ () Int)
(declare-fun _substvar_1445_ () Int)
(declare-fun _substvar_624_ () Int)
(declare-fun _substvar_634_ () Int)
(declare-fun _substvar_1449_ () Int)
(declare-fun _substvar_640_ () Int)
(declare-fun _substvar_1432_ () Int)
(declare-fun _substvar_630_ () Int)
(declare-fun _substvar_1493_ () Int)
(declare-fun _substvar_828_ () Int)
(declare-fun _substvar_622_ () Int)
(declare-fun _substvar_629_ () Int)
(declare-fun _substvar_638_ () Int)
(declare-fun _substvar_627_ () Int)
(declare-fun _substvar_836_ () Int)
(declare-fun _substvar_621_ () Int)
(declare-fun _substvar_628_ () Int)
(declare-fun _substvar_1468_ () Int)
(declare-fun _substvar_832_ () Int)
(declare-fun _substvar_834_ () Int)
(declare-fun _substvar_1464_ () Int)
(declare-fun _substvar_1458_ () Int)
(declare-fun _substvar_633_ () Int)
(declare-fun _substvar_626_ () Int)
(declare-fun _substvar_1180_ () Int)
(declare-fun _substvar_623_ () Int)
(declare-fun _substvar_1429_ () Int)
(declare-fun _substvar_1362_ () Int)
(declare-fun _substvar_620_ () Int)
(declare-fun _substvar_639_ () Int)
(declare-fun _substvar_1410_ () Int)
(declare-fun _substvar_635_ () Int)
(declare-fun _substvar_831_ () Int)
(declare-fun _substvar_637_ () Int)
(declare-fun _substvar_826_ () Int)
(declare-fun _substvar_1809_ () Bool)
(declare-fun _substvar_1501_ () Int)
(declare-fun _substvar_1350_ () Int)
(declare-fun _substvar_833_ () Int)
(declare-fun _substvar_1363_ () Int)
(declare-fun _substvar_1418_ () Int)
(declare-fun _substvar_636_ () Int)
(declare-fun _substvar_1385_ () Int)
(declare-fun _substvar_1783_ () Bool)
(declare-fun _substvar_835_ () Int)
(declare-fun _substvar_642_ () Int)
(declare-fun _substvar_829_ () Int)
(declare-fun _substvar_1446_ () Int)
(declare-fun _substvar_1381_ () Int)
(assert (and (= (+ 0 0 (* (- 1) 0) 0 0 0 0 0 0 0 0 0 0) 0) false))
(assert (or _substvar_1783_ (and (>= _substvar_622_ 0) (>= _substvar_623_ 0) (>= _substvar_624_ 0) (>= _substvar_625_ 0) (>= _substvar_626_ 0) (>= _substvar_627_ 0) (>= _substvar_628_ 0) (>= _substvar_629_ 0) (>= _substvar_630_ 0) (>= _substvar_631_ 0) (>= _substvar_632_ 0) (>= _substvar_633_ 0) (>= _substvar_634_ 0) (>= _substvar_635_ 0) (>= _substvar_636_ 0) (>= _substvar_637_ 0) (> (+ _substvar_1180_ (* 1 _substvar_629_) (* 1 _substvar_630_) _substvar_1349_ _substvar_1350_ (* (- 1) _substvar_633_) (* (- 1) _substvar_634_) 0 (* _substvar_620_ _substvar_636_) (* _substvar_621_ _substvar_637_) (- 1 (+ (+ _substvar_620_ (* 0 1)) 0))) 0) (= (+ _substvar_1362_ _substvar_1363_ (* (- 1) _substvar_624_) _substvar_1366_ (* (- 1) _substvar_629_) (* (- 1) _substvar_630_) (* (- 1) _substvar_633_) (* (- 1) _substvar_634_) _substvar_1375_ 0 0 0 0) 0) (= (+ (* (- 1) _substvar_622_) (* (- 1) _substvar_624_) _substvar_1381_ (* 1 _substvar_628_) (* (- 1) _substvar_631_) _substvar_1385_ (* (- 1) _substvar_634_) 0 0 0 0) 0) (= (+ (* (- 1) _substvar_623_) (* (- 1) _substvar_625_) (* (- 1) _substvar_626_) (* (- 1) _substvar_628_) (* (- 1) _substvar_629_) 0 0 0 0) 0) (= (+ (* (- 1) _substvar_622_) (* (- 1) _substvar_623_) (* (- 1) _substvar_624_) (* (- 1) _substvar_625_) (* (- 1) _substvar_628_) _substvar_1410_ (* (- 1) _substvar_632_) (* (- 1) _substvar_638_) 0 0 0) 0) (= (+ (* (- 1) _substvar_623_) _substvar_1418_ (* (- 1) _substvar_627_) (* 1 _substvar_628_) (* (- 1) _substvar_630_) (* (- 1) _substvar_633_) 0 0 0 0) 0))))
(assert (or _substvar_1809_ (and (>= _substvar_639_ 0) (>= _substvar_640_ 0) (>= _substvar_641_ 0) (>= _substvar_642_ 0) (>= _substvar_643_ 0) (>= _substvar_825_ 0) (>= _substvar_826_ 0) (>= _substvar_827_ 0) (>= _substvar_828_ 0) (>= _substvar_829_ 0) (>= _substvar_830_ 0) (>= _substvar_831_ 0) (>= _substvar_832_ 0) (>= _substvar_833_ 0) (>= _substvar_834_ 0) (>= _substvar_835_ 0) (> (+ _substvar_1429_ (* 1 _substvar_827_) (* 1 _substvar_828_) _substvar_1432_ _substvar_1433_ (* (- 1) _substvar_831_) (* (- 1) _substvar_832_) 0 (* _substvar_620_ _substvar_834_) (* _substvar_621_ _substvar_835_) (- 1 (+ (+ _substvar_621_ (* 0 1)) 0))) 0) (= (+ _substvar_1445_ _substvar_1446_ (* (- 1) _substvar_641_) _substvar_1449_ (* (- 1) _substvar_827_) (* (- 1) _substvar_828_) (* (- 1) _substvar_831_) (* (- 1) _substvar_832_) _substvar_1458_ 0 0 0 0) 0) (= (+ (* (- 1) _substvar_639_) (* (- 1) _substvar_641_) _substvar_1464_ (* 1 _substvar_826_) (* (- 1) _substvar_829_) _substvar_1468_ (* (- 1) _substvar_832_) 0 0 0 0) 0) (= (+ (* (- 1) _substvar_640_) (* (- 1) _substvar_642_) (* (- 1) _substvar_643_) (* (- 1) _substvar_826_) (* (- 1) _substvar_827_) 0 0 0 0) 0) (= (+ (* (- 1) _substvar_639_) (* (- 1) _substvar_640_) (* (- 1) _substvar_641_) (* (- 1) _substvar_642_) (* (- 1) _substvar_826_) _substvar_1493_ (* (- 1) _substvar_830_) (* (- 1) _substvar_836_) 0 0 0) 0) (= (+ (* (- 1) _substvar_640_) _substvar_1501_ (* (- 1) _substvar_825_) (* 1 _substvar_826_) (* (- 1) _substvar_828_) (* (- 1) _substvar_831_) 0 0 0 0) 0))))
(check-sat)
